\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$, ${\it Out}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ (E(${\it Out}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$a$, $b$:E(${\it In}$).\+
\\[0ex]effective($a$)
\\[0ex]$\Rightarrow$ effective($b$)
\\[0ex]$\Rightarrow$ ($\uparrow$(${\it isupdate}$(${\it In}$($a$))))
\\[0ex]$\Rightarrow$ ($\uparrow$(${\it isupdate}$(${\it In}$($b$))))
\\[0ex]$\Rightarrow$ \=(($a$ $\in$ cr{-}explanation\=\{i:l\}\+\+
\\[0ex](${\it es}$; ${\it Sys}$; $f$; $b$))
\-\\[0ex]$\vee$ ($b$ $\in$ cr{-}explanation\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Sys}$; $f$; $a$))))
\-\-\-\\[0ex]$\Rightarrow$ consistent{-}updates(${\it es}$;${\it In}$;${\it Out}$;${\it Cmd}$;${\it isupdate}$;$\lambda$$e$.cr{-}explanation\{i:l\}(${\it es}$; ${\it Sys}$; $f$; $e$)))
\-
\end{tabbing}